$\forall$${\it es}$:ES, $i$, $x$:Id, $T$, $A$:Type, $f$:($T$$\rightarrow$$A$), ${\it Lx}$:(Knd List).
\\[0ex]@$i$ only ${\it Lx}$ affect $x$:$T$
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. (kind($e$) $\in$ ${\it Lx}$) $\Rightarrow$ ($f$(($x$ after $e$)) = $f$($x$ when $e$) $\in$ $A$)
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. $f$($x$ when $e$) = $f$($x$ when es{-}init(${\it es}$;$e$))